# !/usr/bin/env python3
# -*- coding: utf-8 -*-
# @Time : 2023/4/25 14:50
# @Author : xyjiang1216
# @Email : jiangxuyan@nudt.edu.cn
# @File : window_algo_input.py
# @Version: OpenPlanner2.0
from z3 import Array, IntSort, Int

from OpenPlanner.core.api.algo_input_class import Link, Stream, Instance


class GCLLink(Link):
    def __init__(self, **kwargs):
        super().__init__(**kwargs)
        if 'gcl_len' in kwargs:
            self.gcl_len = kwargs['gcl_len']
        else:
            self.gcl_len = 2

        link_id = kwargs['link_id']

        # 下列三个数组是需要SMT求解的未知变量
        # 变量命名规则：
        # Phi/Tau/Kappa^(link_id)： P/T/K区分三个array
        #           i表示link_id
        # 开窗口的时刻的array，即论文中的Phi
        self.phi_array = Array(f'P^({link_id})', IntSort(), IntSort())
        # 关窗口的时刻的array，即论文中的Tau
        self.tau_array = Array(f'T^({link_id})', IntSort(), IntSort())
        # 初始的tau
        self.tau_0_array = Array(f'T_0^({link_id})', IntSort(), IntSort())
        # 存放中间结果的tau
        self.tau_1_array = Array(f'T_1^({link_id})', IntSort(), IntSort())
        # 窗口到队列的映射，即论文中的Kappa
        self.kappa_array = Array(f'K^({link_id})', IntSort(), IntSort())


class GCLStream(Stream):
    def __init__(self, **kwargs):
        super().__init__(**kwargs)
        self.latency_requirement = \
            kwargs['latency_requirement']
        self.jitter_requirement = \
            kwargs['jitter_requirement']


class GCLInstance(Instance):
    def __init__(self,
                 stream_id,
                 period_id,
                 link_id):
        super().__init__(stream_id,
                         period_id,
                         link_id)
        # 即该报文实例对应在Phi和Tau两个array内的索引
        # 对应论文中的Omega
        # Omega也是一个未知数，在初始化的阶段再分配变量名
        # name = 'Omega_' + str(self.stream_id) + ',' + str(self.link_id) \
        #        + '_' + str(self.instance_id)
        self.omega = \
            Int(f'O_{stream_id},{period_id}^({link_id})')